package controller.solver;

import java.io.BufferedReader;
import java.io.IOException;
import java.io.InputStreamReader;

import model.solver.SolverResult;
import model.solver.SolverResultStatus;

/**
 * This Class provide a model for you to add and implement your own solver. 
 * It take care of the maximum of operation so that you only need the give the minimum amount of information and add as quickly as possible your solver.
 * 
 * So to add your preprocessor you only need to implement the hasTimeout method, return false if your solver has no timeout, getCommandLine that return the command line that should be run and also checkParameter that check if everything is fine with the parameter (I recommend to create a new Parameter Class).
 * It also provide you a way to to some additional work after the execution by implementing the returnXXXX method that are call after the execution return the XXXX status.
 * Be aware of the returnProblemCNF method.
 * @author stephane
 *
 */
public abstract class SolverModel extends Solver {


	public static final int RETURN_UNSATISFIABLE = 20;
	public static final int RETURN_SATISFIABLE = 10;

	protected int returnSat = RETURN_SATISFIABLE;
	protected int returnUnSat = RETURN_UNSATISFIABLE;
	protected String description;

	public SolverModel(String description, int sat, int unsat) {
		// TODO Auto-generated constructor stub
		returnSat = sat;
		returnUnSat = unsat;
		this.description = description;
	}

	
	@Override
	public abstract boolean hasTimeout();

	@Override
	public SolverResult runSolver(String[] cmd) {
		SolverResult res = new SolverResult(); 

		BufferedReader input = null;
		BufferedReader inerr = null;
		try{//lance le processus
			res.setBegin(System.currentTimeMillis());
			setRunning(true);

			process = Runtime.getRuntime().exec(cmd);

			String line;
			input = new BufferedReader (new InputStreamReader(process.getInputStream()));
			inerr = new BufferedReader (new InputStreamReader(process.getErrorStream()));

			while ((line = input.readLine()) != null) 
			{ //verifie les stdin
				//System.out.println(line);
				res.addStdin(line+"\n");
			}
			while ((line = inerr.readLine()) != null) 
			{ //verifie les stderr
				//System.out.println(line);
				res.addStderr(line+"\n");
			}
		}
		catch(IOException e){
			//e.printStackTrace();
			res.setStatus(SolverResultStatus.PROBLEM);
			if(process != null)
				process.destroy();
		}
		finally{
			try{
				if(input != null)
					input.close();
				if(inerr != null)
					inerr.close();
				if(process != null)
					res.setExitVal(process.waitFor());
			}
			catch(Exception e){
				//e.printStackTrace();
				res.setStatus(SolverResultStatus.PROBLEM);
			}
			finally{
				setRunning(false);
			}
		}
		//terminer
		res.setEnd(System.currentTimeMillis());

		//System.out.println("val de retour"+res.getExitVal());

		//dernier details
		res.setDescription(description);
		
		//s'occupe du status
		if(hasBeenStop()) 
		{//cas timeout
			res.setStatus(SolverResultStatus.TIMEOUT_REACHED);
			returnHasBeenStop(res);
		}
		else
			if(res.getStatus() == SolverResultStatus.PROBLEM)
				if(res.getExitVal() == returnUnSat)
				{//UNSAT
					res.setStatus(SolverResultStatus.UNSATISFIABLE) ;
					returnUnSat(res);
				}
				else
					if(res.getExitVal() == returnSat)
					{ //SAT
						res.setStatus(SolverResultStatus.SATISFIABLE) ; 
						returnSat(res);
					}
					else
					{					
						res.setStatus(SolverResultStatus.PROBLEM) ;
						returnProblem(res);
					}

		return res;
	}

	/**
	 * is call when the result after the execution of the solver is SAT
	 * @param res the actual result of the solving
	 */
	protected abstract void returnSat(SolverResult res);
	/**
	 * is call when the result after the execution of the solver is UNSAT
	 * @param res the actual result of the solving
	 */
	protected abstract void returnUnSat(SolverResult res);
	/**
	 * is call when there was a problem
	 * @param res the actual result of the solving
	 */
	protected abstract void returnProblem(SolverResult res);
	/**
	 * is call after the execution of the solver has been stop by the timeout
	 * @param res the actual result of the solving
	 */
	protected abstract void returnHasBeenStop(SolverResult res);

	@Override
	public abstract String[] getCommandLine(String cnfFile);

}
